package com.graphcoloring;

import org.sat4j.core.VecInt;
import org.sat4j.minisat.SolverFactory;
import org.sat4j.specs.ISolver;

import java.util.List;
import java.util.Set;

/**
 * Created by IntelliJ IDEA.
 * User: martin
 * Date: 11/23/11
 * Time: 6:25 PM
 * To change this template use File | Settings | File Templates.
 */
public class ExplicitBitwiseSolver implements Solver {

    public Solution solve(GraphInputData inputData) throws Exception {

        int n = inputData.getVertexNumber();
        List<Integer[]> edges = inputData.getEdgeList();

        int colorsCount = n;
        int edgeCount = edges.size();
        int colors[] = new int[n];


        for (int k = n; k >= 1; k--) {
            int l = (int) Math.ceil((Math.log(k) / Math.log(2)));

            if (k == 1) {
                Solution solution = new Solution();
                solution.colorCount = colorsCount;
                solution.colors = colors;
                return solution;
            }

            ISolver solver = SolverFactory.newDefault();
            solver.setTimeout(60);
            solver.newVar((l * (n + 1)) + (l * edgeCount));


            int currentEdge = 0;
            for (Integer[] edge : edges) {
                int vertex1 = edge[0] + 1;
                int vertex2 = edge[1] + 1;

                int[] xvars = new int[l];      // names of the variables corresponding to bits of vertex 1
                int[] yvars = new int[l];
                int[] xorvar = new int[l];

                for (int i = 0; i < l; ++i) {
                    xvars[i] = vertex1 * l + i;
                    yvars[i] = vertex2 * l + i;
                    xorvar[i] = (l * (n + 1)) + (currentEdge * l + i);
                }
                currentEdge++;
                for (int i = 0; i < l; i++) {

                    solver.addClause(new VecInt(new int[]
                            {xvars[i], yvars[i], -xorvar[i]}));
                    solver.addClause(new VecInt(new int[]
                            {-xvars[i], -yvars[i], -xorvar[i]}));
                    solver.addClause(new VecInt(new int[]
                            {-xvars[i], yvars[i], xorvar[i]}));
                    solver.addClause(new VecInt(new int[]
                            {xvars[i], -yvars[i], xorvar[i]}));
                }
                solver.addClause(new VecInt(xorvar));

            }
            Set<Integer> vertices = inputData.getConnectedEdges().keySet();

            for (int vertice : vertices) {
                for (int i = k; i < Math.pow(2, l); i++) {
                    int[] clause = new int[l];
                    int var = vertice + 1;
                    int j = i;

                    int[] bits = new int[l];
                    int pos = 0;
                    while (j != 0) {
                        bits[pos] = j % 2;
                        j = j / 2;
                        pos++;
                    }
                    for (int b = 0; b < l; b++) {
                        if (bits[b] == 0) {
                            clause[b] = var * l + b;
                        } else {
                            clause[b] = -(var * l + b);
                        }

                    }
                    solver.addClause(new VecInt(clause));

                }
            }


            if (solver.isSatisfiable()) {
                int model[] = solver.model();
                colorsCount = k;
                for (int vertex = 0; vertex < n; ++vertex) {
                    int color = 0, mult = 1;
                    for (int bit = 0; bit < l; ++bit) {
                        if (model[vertex * l + bit] > 0) color += mult;
                        mult *= 2;
                    }
                    colors[vertex] = color;
                }
            } else {
                Solution solution = new Solution();
                solution.colorCount = colorsCount;
                solution.colors = colors;
                return solution;
            }

        }
        return null;

    }

}
